$\forall$$T$:Type, $l$, ${\it l'}$:($T$ List). l\_disjoint($T$;$l$;${\it l'}$) $\in$ $\mathbb{P}$